Nuprl Lemma : implies-es-atom-axiom 0,22

es:ES, T:(i:Idk:Kndkindtype(i;k)state@istate@i),
S:(i:Idk:Kndkindtype(i;k)state@i(Msg List)),
C:(i,b:Idstate@i(kindtype(i;locl(b))+Unit)).
(e:E. state after e = T(loc(e),kind(e),val(e),(state when e)))
& (e:E.
& (islocal(kind(e))
& ( isl(C(loc(e),act(kind(e)),(state when e)))
& ( & val(e) = outl(C(loc(e),act(kind(e)),(state when e)))  valtype(e))
& (e:E.
& (isrcv(kind(e))
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  S
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  (loc(sender(e))
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  ,kind(sender(e))
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  ,val(sender(e))
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  ,(state when sender(e)))))
 (a:Atom1, e:E.
 (((state when e):state@loc(e)>>a
 (( first(e)
 (( T(loc(e)):k:Kndkindtype(loc(e);k)state@loc(e)state@loc(e)>>a
 ((  C(loc(e)):b:Idstate@loc(e)(kindtype(loc(e);locl(b))+Unit)>>a
 ((  (state when pred(e)):state@loc(pred(e))>>a
 ((  isrcv(pred(e)) & val(pred(e)):valtype(pred(e))>>a)
 (& (e sends a
 (& ( S(loc(e)):k:Kndkindtype(loc(e);k)state@loc(e)(Msg List)>>a
 (& (  C(loc(e)):b:Idstate@loc(e)(kindtype(loc(e);locl(b))+Unit)>>a
 (& (  (state when e):state@loc(e)>>a
 (& (  isrcv(e) & val(e):valtype(e)>>a)) 
latex


Definitionsx:AB(x), P  Q, P & Q, A & B, isrcv(e), t  T, Prop, Top, S  T, P  Q, P  Q, t  ...$L, T, True, P  Q, xt(x), SQType(T), {T}, b, islocal(k), isl(x), act(k), b, outr(x), true, false, if b t else f fi, x:AB(x), Msg, emsg(e), Msg(M), msg(l;t;v), valtype(e), False, SqStable(P), x(s), Dec(P), Knd, e sends a, e receives a, Unit, , A, locl(a), lnk(e), tag(e), rcvtype(e),
Lemmasnot wf, assert wf, es-first wf, inheres wf, es-state wf, es-loc wf, es-state-when wf, atom-free-es-state, es-send-atom wf, es-E wf, es-state-after wf, es-kind wf, es-valtype-kindtype, es-val wf, islocal wf, isl wf, es-kindtype wf, locl wf, actof wf, unit wf, es-valtype wf, outl wf, isrcv wf, l member wf, es-Msg wf, es-sender wf, Id wf, Knd wf, event system wf, es-pred wf, state-after-pred, squash wf, true wf, es-loc-pred, inherence-ap-elim, atom-free-es-valtype, atom-free-Knd, atom-free-es-kindtype, inherence-trivial, sq stable atom-free, atom-free-es-Msg, atom-free-function, atom-free-settype, Knd sq, atom-free wf, atom-free-dep-function, atom-free-Id, decidable assert, es-isrcv wf, islocal-not-isrcv, assert of bnot, outl-inherence, false wf, atom-free-union, Id sq, subtype rel self, sq stable subtype rel, list-inherence, es-msg wf, atom-free-list, lnk wf, tagof wf, bool wf, eqtt to assert, es-rcvtype wf, iff transitivity, bnot wf, eqff to assert, es-M wf

origin